A, B:Realizer. A  B  R-Feasible(B)  R-Feasible(A) 

latex

Definitions

P & Q, if b then t else f fi , ff, tt, x. t(x), Rnone?(x1), b, True, R-Feasible(R), i  j , False, A, A  B, {T}, SQType(T), , t  T, P  Q, x:A. B(x), x(s), Unit, Realizer, , P  Q, P  Q, Y, , A  B, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),

Lemmas

R-sub-compat, Rplus-right wf, Rplus-left wf, Rplus-implies, R-size-decreases, Rplus? wf, false wf, true wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, ge wf, nat properties, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, Rnone? wf, bool cases, es realizer wf, nat plus wf, le wf, R-sub wf, R-Feasible wf, R-size wf, nat wf